(set-logic QF_UFLRA)
(set-info :source |CPAchecker with bounded model checking on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")


(define-fun _2 () Bool false)
(declare-fun personOnFloor_2_0@2 () Real)
(declare-fun |buttonForFloorIsPressed::floorID@2| () Real)
(declare-fun __ADDRESS_OF_floorButtons_2 () Real)
(declare-fun |__ADDRESS_OF_stopRequestedInDirection__wrappee__base::tmp___9| () Real)
(declare-fun |__ADDRESS_OF_timeShift::tmp___2| () Real)
(declare-fun |isFloorCalling::__retval__@2| () Real)
(declare-fun |stopRequestedInDirection::respectFloorCalls@2| () Real)
(declare-fun |getOrigin::retValue_acc@3| () Real)
(declare-fun |stopRequestedInDirection::tmp___0@3| () Real)
(declare-fun __ADDRESS_OF_floorButtons_4 () Real)
(declare-fun |isTopFloor::retValue_acc@3| () Real)
(declare-fun |isFloorCalling::retValue_acc@5| () Real)
(declare-fun |__ADDRESS_OF_stopRequestedInDirection::__cil_tmp8| () Real)
(declare-fun __ADDRESS_OF_calls_2 () Real)
(declare-fun |isFloorCalling::floorID@2| () Real)
(declare-fun |stopRequestedInDirection__wrappee__base::respectInLiftCalls@2| () Real)
(declare-fun __ADDRESS_OF_personOnFloor_4_2 () Real)
(declare-fun __ADDRESS_OF_persons_5 () Real)
(declare-fun __ADDRESS_OF_calls_4 () Real)
(declare-fun __ADDRESS_OF_personOnFloor_5_4 () Real)
(declare-fun floorButtons_0@2 () Real)
(declare-fun ___pc@3 () Real)
(declare-fun __ADDRESS_OF_calls_0 () Real)
(declare-fun |__ADDRESS_OF_stopRequestedInDirection__wrappee__base::tmp___2| () Real)
(declare-fun personOnFloor_3_3@2 () Real)
(declare-fun |isFloorCalling::__retval__@4| () Real)
(declare-fun __BASE_ADDRESS_OF__ (Real) Real)
(declare-fun __ADDRESS_OF_floorButtons_1 () Real)
(declare-fun __ADDRESS_OF_personOnFloor_0_3 () Real)
(declare-fun __ADDRESS_OF_personOnFloor_2_2 () Real)
(declare-fun personOnFloor_0_2@2 () Real)
(declare-fun __ADDRESS_OF_personOnFloor_2_4 () Real)
(declare-fun personOnFloor_1_1@2 () Real)
(declare-fun |isTopFloor::floorID@2| () Real)
(declare-fun floorButtons_3@2 () Real)
(declare-fun doorState@3 () Real)
(declare-fun |callOnFloor::floorID@2| () Real)
(declare-fun personOnFloor_4_4@2 () Real)
(declare-fun |initPersonOnFloor::floor@2| () Real)
(declare-fun __ADDRESS_OF_personOnFloor_1_3 () Real)
(declare-fun |stopRequestedInDirection__wrappee__base::dir@2| () Real)
(declare-fun calls_1@2 () Real)
(declare-fun |__ADDRESS_OF_stopRequestedInDirection__wrappee__base::tmp___7| () Real)
(declare-fun personOnFloor_5_1@2 () Real)
(declare-fun __ADDRESS_OF_currentFloorID () Real)
(declare-fun |initPersonOnFloor::person@2| () Real)
(declare-fun personOnFloor_5_3@2 () Real)
(declare-fun |__ADDRESS_OF_timeShift::tmp___8| () Real)
(declare-fun personOnFloor_4_3@2 () Real)
(declare-fun __ADDRESS_OF_personOnFloor_4_0 () Real)
(declare-fun persons_4@2 () Real)
(declare-fun |getOrigin::person@2| () Real)
(declare-fun calls_3@2 () Real)
(declare-fun personOnFloor_4_0@2 () Real)
(declare-fun |__ADDRESS_OF_stopRequestedAtCurrentFloor::tmp___0| () Real)
(declare-fun doorState@2 () Real)
(declare-fun |__ADDRESS_OF_getOrigin::retValue_acc| () Real)
(declare-fun |__ADDRESS_OF_stopRequestedAtCurrentFloor__wrappee__base::tmp___0| () Real)
(declare-fun __ADDRESS_OF_persons_3 () Real)
(declare-fun |__ADDRESS_OF_stopRequestedInDirection__wrappee__base::tmp___0| () Real)
(declare-fun __ADDRESS_OF_personOnFloor_3_1 () Real)
(declare-fun |__ADDRESS_OF_timeShift::tmp___5| () Real)
(declare-fun personOnFloor_2_3@2 () Real)
(declare-fun __ADDRESS_OF_personOnFloor_2_0 () Real)
(declare-fun personOnFloor_1_2@2 () Real)
(declare-fun |stopRequestedInDirection__wrappee__base::tmp@3| () Real)
(declare-fun |__ADDRESS_OF_stopRequestedInDirection::tmp___0| () Real)
(declare-fun |isExecutiveFloorCalling::retValue_acc@3| () Real)
(declare-fun |__ADDRESS_OF_timeShift::tmp___3| () Real)
(declare-fun currentHeading@2 () Real)
(declare-fun |__ADDRESS_OF_stopRequestedAtCurrentFloor::retValue_acc| () Real)
(declare-fun __ADDRESS_OF_personOnFloor_0_0 () Real)
(declare-fun personOnFloor_5_0@2 () Real)
(declare-fun |stopRequestedAtCurrentFloor__wrappee__base::retValue_acc@3| () Real)
(declare-fun |isFloorCalling::__retval__@3| () Real)
(declare-fun |isTopFloor::__retval__@2| () Real)
(declare-fun __ADDRESS_OF_personOnFloor_1_0 () Real)
(declare-fun |stopRequestedAtCurrentFloor::retValue_acc@3| () Real)
(declare-fun |__ADDRESS_OF_main::tmp| () Real)
(declare-fun |stopRequestedAtCurrentFloor__wrappee__base::tmp@3| () Real)
(declare-fun floorButtons_2@2 () Real)
(declare-fun personOnFloor_0_4@2 () Real)
(declare-fun |__ADDRESS_OF_bigMacCall::tmp| () Real)
(declare-fun |__ADDRESS_OF_stopRequestedInDirection__wrappee__base::tmp___5| () Real)
(declare-fun __ADDRESS_OF_personOnFloor_5_1 () Real)
(declare-fun cleanupTimeShifts@2 () Real)
(declare-fun |__ADDRESS_OF_stopRequestedInDirection::retValue_acc| () Real)
(declare-fun |__ADDRESS_OF_timeShift::tmp___0| () Real)
(declare-fun |__ADDRESS_OF_stopRequestedAtCurrentFloor__wrappee__base::retValue_acc| () Real)
(declare-fun __ADDRESS_OF_personOnFloor_3_3 () Real)
(declare-fun personOnFloor_3_0@2 () Real)
(declare-fun |isExecutiveFloorCalling::retValue_acc@5| () Real)
(declare-fun |valid_product::retValue_acc@3| () Real)
(declare-fun |stopRequestedAtCurrentFloor__wrappee__base::tmp___0@3| () Real)
(declare-fun persons_2@2 () Real)
(declare-fun __ADDRESS_OF_executiveFloor () Real)
(declare-fun personOnFloor_1_4@2 () Real)
(declare-fun __ADDRESS_OF_calls_1 () Real)
(declare-fun __ADDRESS_OF_persons_0 () Real)
(declare-fun __ADDRESS_OF_personOnFloor_0_2 () Real)
(declare-fun |__ADDRESS_OF_stopRequestedInDirection__wrappee__base::retValue_acc| () Real)
(declare-fun __ADDRESS_OF_floorButtons_3 () Real)
(declare-fun |stopRequestedInDirection::dir@2| () Real)
(declare-fun |isFloorCalling::floorID@4| () Real)
(declare-fun |__ADDRESS_OF_stopRequestedInDirection__wrappee__base::tmp___3| () Real)
(declare-fun __ADDRESS_OF_personOnFloor_5_3 () Real)
(declare-fun |__ADDRESS_OF_timeShift::tmp___9| () Real)
(declare-fun __ADDRESS_OF_personOnFloor_4_3 () Real)
(declare-fun |isExecutiveFloorCalling::__retval__@2| () Real)
(declare-fun personOnFloor_3_2@2 () Real)
(declare-fun __ADDRESS_OF_floorButtons_0 () Real)
(declare-fun __ADDRESS_OF_persons_4 () Real)
(declare-fun __ADDRESS_OF_calls_3 () Real)
(declare-fun personOnFloor_2_1@2 () Real)
(declare-fun __ADDRESS_OF_doorState () Real)
(declare-fun personOnFloor_0_0@2 () Real)
(declare-fun calls_1@3 () Real)
(declare-fun |__ADDRESS_OF_isExecutiveFloorCalling::retValue_acc| () Real)
(declare-fun personOnFloor_0_1@2 () Real)
(declare-fun |__ADDRESS_OF_timeShift::tmp___6| () Real)
(declare-fun personOnFloor_4_1@2 () Real)
(declare-fun __ADDRESS_OF_personOnFloor_2_3 () Real)
(declare-fun personOnFloor_1_0@2 () Real)
(declare-fun |__ADDRESS_OF_stopRequestedInDirection__wrappee__base::tmp___8| () Real)
(declare-fun calls_0@2 () Real)
(declare-fun __ADDRESS_OF_personOnFloor_1_2 () Real)
(declare-fun |__ADDRESS_OF_isTopFloor::retValue_acc| () Real)
(declare-fun |__ADDRESS_OF_timeShift::tmp___4| () Real)
(declare-fun __ADDRESS_OF_currentHeading () Real)
(declare-fun __ADDRESS_OF_personOnFloor_5_0 () Real)
(declare-fun personOnFloor_5_2@2 () Real)
(declare-fun |stopRequestedInDirection__wrappee__base::respectFloorCalls@2| () Real)
(declare-fun personOnFloor_3_4@2 () Real)
(declare-fun |buttonForFloorIsPressed::retValue_acc@3| () Real)
(declare-fun __ADDRESS_OF_personOnFloor_0_4 () Real)
(declare-fun |__ADDRESS_OF_stopRequestedInDirection::__cil_tmp7| () Real)
(declare-fun |getOrigin::__retval__@2| () Real)
(declare-fun |__ADDRESS_OF_stopRequestedInDirection__wrappee__base::tmp___1| () Real)
(declare-fun __ADDRESS_OF_cleanupTimeShifts () Real)
(declare-fun |__ADDRESS_OF_buttonForFloorIsPressed::retValue_acc| () Real)
(declare-fun persons_3@2 () Real)
(declare-fun personOnFloor_5_1@3 () Real)
(declare-fun |__ADDRESS_OF_timeShift::tmp___1| () Real)
(declare-fun |isFloorCalling::retValue_acc@3| () Real)
(declare-fun calls_2@2 () Real)
(declare-fun personOnFloor_0_3@2 () Real)
(declare-fun |stopRequestedAtCurrentFloor::__retval__@2| () Real)
(declare-fun __ADDRESS_OF_personOnFloor_3_0 () Real)
(declare-fun |isExecutiveFloorCalling::__retval__@3| () Real)
(declare-fun |valid_product::__retval__@2| () Real)
(declare-fun |isFloorCalling::floorID@3| () Real)
(declare-fun floorButtons_4@2 () Real)
(declare-fun persons_5@2 () Real)
(declare-fun calls_4@2 () Real)
(declare-fun |__ADDRESS_OF_isFloorCalling::retValue_acc| () Real)
(declare-fun __ADDRESS_OF_personOnFloor_1_4 () Real)
(declare-fun personOnFloor_4_2@2 () Real)
(declare-fun personOnFloor_5_4@2 () Real)
(declare-fun |__ADDRESS_OF_stopRequestedInDirection__wrappee__base::tmp___6| () Real)
(declare-fun floorButtons_1@2 () Real)
(declare-fun |isFloorCalling::retValue_acc@7| () Real)
(declare-fun __ADDRESS_OF_persons_1 () Real)
(declare-fun __ADDRESS_OF_personOnFloor_4_4 () Real)
(declare-fun personOnFloor_2_2@2 () Real)
(declare-fun |bigMacCall::tmp@3| () Real)
(declare-fun |stopRequestedAtCurrentFloor::tmp@3| () Real)
(declare-fun |stopRequestedInDirection::respectInLiftCalls@2| () Real)
(declare-fun __ADDRESS_OF_personOnFloor_3_2 () Real)
(declare-fun ___pc@4 () Real)
(declare-fun personOnFloor_2_4@2 () Real)
(declare-fun |__ADDRESS_OF_stopRequestedAtCurrentFloor__wrappee__base::tmp| () Real)
(declare-fun |timeShift::tmp___9@3| () Real)
(declare-fun |__ADDRESS_OF_stopRequestedAtCurrentFloor::tmp| () Real)
(declare-fun |__ADDRESS_OF_stopRequestedInDirection__wrappee__base::tmp| () Real)
(declare-fun __ADDRESS_OF_personOnFloor_2_1 () Real)
(declare-fun personOnFloor_1_3@2 () Real)
(declare-fun |main::tmp@3| () Real)
(declare-fun currentFloorID@2 () Real)
(declare-fun |__ADDRESS_OF_timeShift::tmp| () Real)
(declare-fun __ADDRESS_OF_personOnFloor_0_1 () Real)
(declare-fun executiveFloor@2 () Real)
(declare-fun |__ADDRESS_OF_timeShift::tmp___7| () Real)
(declare-fun __ADDRESS_OF_personOnFloor_1_1 () Real)
(declare-fun persons_1@2 () Real)
(declare-fun __ADDRESS_OF_personOnFloor_4_1 () Real)
(declare-fun __ADDRESS_OF_personOnFloor_5_2 () Real)
(declare-fun |__ADDRESS_OF_valid_product::retValue_acc| () Real)
(declare-fun persons_0@2 () Real)
(declare-fun |__ADDRESS_OF_stopRequestedInDirection::tmp| () Real)
(declare-fun |__ADDRESS_OF_stopRequestedInDirection__wrappee__base::tmp___4| () Real)
(declare-fun __ADDRESS_OF_personOnFloor_3_4 () Real)
(declare-fun |buttonForFloorIsPressed::__retval__@2| () Real)
(declare-fun personOnFloor_3_1@2 () Real)
(declare-fun __ADDRESS_OF____pc () Real)
(declare-fun __ADDRESS_OF_persons_2 () Real)
(declare-fun |stopRequestedAtCurrentFloor__wrappee__base::__retval__@2| () Real)
(define-fun _7 () Real 0)
(define-fun _8 () Real __ADDRESS_OF____pc)
(define-fun _9 () Real (__BASE_ADDRESS_OF__ _8))
(define-fun _10 () Bool (= _8 _9))
(define-fun _11 () Real ___pc@3)
(define-fun _12 () Bool (= _11 _7))
(define-fun _13 () Bool (and _10 _12))
(define-fun _14 () Real 17)
(define-fun _15 () Bool (= _11 _14))
(define-fun _16 () Real 1)
(define-fun _18 () Bool (not _15))
(define-fun _19 () Bool (and _13 _18))
(define-fun _21 () Bool (and _12 _19))
(define-fun _24 () Real __ADDRESS_OF_executiveFloor)
(define-fun _25 () Real (__BASE_ADDRESS_OF__ _24))
(define-fun _26 () Bool (= _24 _25))
(define-fun _27 () Real 4)
(define-fun _28 () Real executiveFloor@2)
(define-fun _29 () Bool (= _28 _27))
(define-fun _30 () Bool (and _26 _29))
(define-fun _31 () Bool (and _21 _30))
(define-fun _32 () Real __ADDRESS_OF_cleanupTimeShifts)
(define-fun _33 () Real (__BASE_ADDRESS_OF__ _32))
(define-fun _34 () Bool (= _32 _33))
(define-fun _35 () Real 12)
(define-fun _36 () Real cleanupTimeShifts@2)
(define-fun _37 () Bool (= _36 _35))
(define-fun _38 () Bool (and _34 _37))
(define-fun _39 () Bool (and _31 _38))
(define-fun _40 () Real __ADDRESS_OF_calls_0)
(define-fun _41 () Real (__BASE_ADDRESS_OF__ _40))
(define-fun _42 () Bool (= _40 _41))
(define-fun _43 () Real calls_0@2)
(define-fun _44 () Bool (= _43 _7))
(define-fun _45 () Bool (and _42 _44))
(define-fun _46 () Bool (and _39 _45))
(define-fun _47 () Real __ADDRESS_OF_calls_1)
(define-fun _48 () Real (__BASE_ADDRESS_OF__ _47))
(define-fun _49 () Bool (= _47 _48))
(define-fun _50 () Real calls_1@2)
(define-fun _51 () Bool (= _50 _7))
(define-fun _52 () Bool (and _49 _51))
(define-fun _53 () Bool (and _46 _52))
(define-fun _54 () Real __ADDRESS_OF_calls_2)
(define-fun _55 () Real (__BASE_ADDRESS_OF__ _54))
(define-fun _56 () Bool (= _54 _55))
(define-fun _57 () Real calls_2@2)
(define-fun _58 () Bool (= _57 _7))
(define-fun _59 () Bool (and _56 _58))
(define-fun _60 () Bool (and _53 _59))
(define-fun _61 () Real __ADDRESS_OF_calls_3)
(define-fun _62 () Real (__BASE_ADDRESS_OF__ _61))
(define-fun _63 () Bool (= _61 _62))
(define-fun _64 () Real calls_3@2)
(define-fun _65 () Bool (= _64 _7))
(define-fun _66 () Bool (and _63 _65))
(define-fun _67 () Bool (and _60 _66))
(define-fun _68 () Real __ADDRESS_OF_calls_4)
(define-fun _69 () Real (__BASE_ADDRESS_OF__ _68))
(define-fun _70 () Bool (= _68 _69))
(define-fun _71 () Real calls_4@2)
(define-fun _72 () Bool (= _71 _7))
(define-fun _73 () Bool (and _70 _72))
(define-fun _74 () Bool (and _67 _73))
(define-fun _75 () Real __ADDRESS_OF_personOnFloor_0_0)
(define-fun _76 () Real (__BASE_ADDRESS_OF__ _75))
(define-fun _77 () Bool (= _75 _76))
(define-fun _78 () Real personOnFloor_0_0@2)
(define-fun _79 () Bool (= _78 _7))
(define-fun _80 () Bool (and _77 _79))
(define-fun _81 () Bool (and _74 _80))
(define-fun _82 () Real __ADDRESS_OF_personOnFloor_0_1)
(define-fun _83 () Real (__BASE_ADDRESS_OF__ _82))
(define-fun _84 () Bool (= _82 _83))
(define-fun _85 () Real personOnFloor_0_1@2)
(define-fun _86 () Bool (= _85 _7))
(define-fun _87 () Bool (and _84 _86))
(define-fun _88 () Bool (and _81 _87))
(define-fun _89 () Real __ADDRESS_OF_personOnFloor_0_2)
(define-fun _90 () Real (__BASE_ADDRESS_OF__ _89))
(define-fun _91 () Bool (= _89 _90))
(define-fun _92 () Real personOnFloor_0_2@2)
(define-fun _93 () Bool (= _92 _7))
(define-fun _94 () Bool (and _91 _93))
(define-fun _95 () Bool (and _88 _94))
(define-fun _96 () Real __ADDRESS_OF_personOnFloor_0_3)
(define-fun _97 () Real (__BASE_ADDRESS_OF__ _96))
(define-fun _98 () Bool (= _96 _97))
(define-fun _99 () Real personOnFloor_0_3@2)
(define-fun _100 () Bool (= _99 _7))
(define-fun _101 () Bool (and _98 _100))
(define-fun _102 () Bool (and _95 _101))
(define-fun _103 () Real __ADDRESS_OF_personOnFloor_0_4)
(define-fun _104 () Real (__BASE_ADDRESS_OF__ _103))
(define-fun _105 () Bool (= _103 _104))
(define-fun _106 () Real personOnFloor_0_4@2)
(define-fun _107 () Bool (= _106 _7))
(define-fun _108 () Bool (and _105 _107))
(define-fun _109 () Bool (and _102 _108))
(define-fun _110 () Real __ADDRESS_OF_personOnFloor_1_0)
(define-fun _111 () Real (__BASE_ADDRESS_OF__ _110))
(define-fun _112 () Bool (= _110 _111))
(define-fun _113 () Real personOnFloor_1_0@2)
(define-fun _114 () Bool (= _113 _7))
(define-fun _115 () Bool (and _112 _114))
(define-fun _116 () Bool (and _109 _115))
(define-fun _117 () Real __ADDRESS_OF_personOnFloor_1_1)
(define-fun _118 () Real (__BASE_ADDRESS_OF__ _117))
(define-fun _119 () Bool (= _117 _118))
(define-fun _120 () Real personOnFloor_1_1@2)
(define-fun _121 () Bool (= _120 _7))
(define-fun _122 () Bool (and _119 _121))
(define-fun _123 () Bool (and _116 _122))
(define-fun _124 () Real __ADDRESS_OF_personOnFloor_1_2)
(define-fun _125 () Real (__BASE_ADDRESS_OF__ _124))
(define-fun _126 () Bool (= _124 _125))
(define-fun _127 () Real personOnFloor_1_2@2)
(define-fun _128 () Bool (= _127 _7))
(define-fun _129 () Bool (and _126 _128))
(define-fun _130 () Bool (and _123 _129))
(define-fun _131 () Real __ADDRESS_OF_personOnFloor_1_3)
(define-fun _132 () Real (__BASE_ADDRESS_OF__ _131))
(define-fun _133 () Bool (= _131 _132))
(define-fun _134 () Real personOnFloor_1_3@2)
(define-fun _135 () Bool (= _134 _7))
(define-fun _136 () Bool (and _133 _135))
(define-fun _137 () Bool (and _130 _136))
(define-fun _138 () Real __ADDRESS_OF_personOnFloor_1_4)
(define-fun _139 () Real (__BASE_ADDRESS_OF__ _138))
(define-fun _140 () Bool (= _138 _139))
(define-fun _141 () Real personOnFloor_1_4@2)
(define-fun _142 () Bool (= _141 _7))
(define-fun _143 () Bool (and _140 _142))
(define-fun _144 () Bool (and _137 _143))
(define-fun _145 () Real __ADDRESS_OF_personOnFloor_2_0)
(define-fun _146 () Real (__BASE_ADDRESS_OF__ _145))
(define-fun _147 () Bool (= _145 _146))
(define-fun _148 () Real personOnFloor_2_0@2)
(define-fun _149 () Bool (= _148 _7))
(define-fun _150 () Bool (and _147 _149))
(define-fun _151 () Bool (and _144 _150))
(define-fun _152 () Real __ADDRESS_OF_personOnFloor_2_1)
(define-fun _153 () Real (__BASE_ADDRESS_OF__ _152))
(define-fun _154 () Bool (= _152 _153))
(define-fun _155 () Real personOnFloor_2_1@2)
(define-fun _156 () Bool (= _155 _7))
(define-fun _157 () Bool (and _154 _156))
(define-fun _158 () Bool (and _151 _157))
(define-fun _159 () Real __ADDRESS_OF_personOnFloor_2_2)
(define-fun _160 () Real (__BASE_ADDRESS_OF__ _159))
(define-fun _161 () Bool (= _159 _160))
(define-fun _162 () Real personOnFloor_2_2@2)
(define-fun _163 () Bool (= _162 _7))
(define-fun _164 () Bool (and _161 _163))
(define-fun _165 () Bool (and _158 _164))
(define-fun _166 () Real __ADDRESS_OF_personOnFloor_2_3)
(define-fun _167 () Real (__BASE_ADDRESS_OF__ _166))
(define-fun _168 () Bool (= _166 _167))
(define-fun _169 () Real personOnFloor_2_3@2)
(define-fun _170 () Bool (= _169 _7))
(define-fun _171 () Bool (and _168 _170))
(define-fun _172 () Bool (and _165 _171))
(define-fun _173 () Real __ADDRESS_OF_personOnFloor_2_4)
(define-fun _174 () Real (__BASE_ADDRESS_OF__ _173))
(define-fun _175 () Bool (= _173 _174))
(define-fun _176 () Real personOnFloor_2_4@2)
(define-fun _177 () Bool (= _176 _7))
(define-fun _178 () Bool (and _175 _177))
(define-fun _179 () Bool (and _172 _178))
(define-fun _180 () Real __ADDRESS_OF_personOnFloor_3_0)
(define-fun _181 () Real (__BASE_ADDRESS_OF__ _180))
(define-fun _182 () Bool (= _180 _181))
(define-fun _183 () Real personOnFloor_3_0@2)
(define-fun _184 () Bool (= _183 _7))
(define-fun _185 () Bool (and _182 _184))
(define-fun _186 () Bool (and _179 _185))
(define-fun _187 () Real __ADDRESS_OF_personOnFloor_3_1)
(define-fun _188 () Real (__BASE_ADDRESS_OF__ _187))
(define-fun _189 () Bool (= _187 _188))
(define-fun _190 () Real personOnFloor_3_1@2)
(define-fun _191 () Bool (= _190 _7))
(define-fun _192 () Bool (and _189 _191))
(define-fun _193 () Bool (and _186 _192))
(define-fun _194 () Real __ADDRESS_OF_personOnFloor_3_2)
(define-fun _195 () Real (__BASE_ADDRESS_OF__ _194))
(define-fun _196 () Bool (= _194 _195))
(define-fun _197 () Real personOnFloor_3_2@2)
(define-fun _198 () Bool (= _197 _7))
(define-fun _199 () Bool (and _196 _198))
(define-fun _200 () Bool (and _193 _199))
(define-fun _201 () Real __ADDRESS_OF_personOnFloor_3_3)
(define-fun _202 () Real (__BASE_ADDRESS_OF__ _201))
(define-fun _203 () Bool (= _201 _202))
(define-fun _204 () Real personOnFloor_3_3@2)
(define-fun _205 () Bool (= _204 _7))
(define-fun _206 () Bool (and _203 _205))
(define-fun _207 () Bool (and _200 _206))
(define-fun _208 () Real __ADDRESS_OF_personOnFloor_3_4)
(define-fun _209 () Real (__BASE_ADDRESS_OF__ _208))
(define-fun _210 () Bool (= _208 _209))
(define-fun _211 () Real personOnFloor_3_4@2)
(define-fun _212 () Bool (= _211 _7))
(define-fun _213 () Bool (and _210 _212))
(define-fun _214 () Bool (and _207 _213))
(define-fun _215 () Real __ADDRESS_OF_personOnFloor_4_0)
(define-fun _216 () Real (__BASE_ADDRESS_OF__ _215))
(define-fun _217 () Bool (= _215 _216))
(define-fun _218 () Real personOnFloor_4_0@2)
(define-fun _219 () Bool (= _218 _7))
(define-fun _220 () Bool (and _217 _219))
(define-fun _221 () Bool (and _214 _220))
(define-fun _222 () Real __ADDRESS_OF_personOnFloor_4_1)
(define-fun _223 () Real (__BASE_ADDRESS_OF__ _222))
(define-fun _224 () Bool (= _222 _223))
(define-fun _225 () Real personOnFloor_4_1@2)
(define-fun _226 () Bool (= _225 _7))
(define-fun _227 () Bool (and _224 _226))
(define-fun _228 () Bool (and _221 _227))
(define-fun _229 () Real __ADDRESS_OF_personOnFloor_4_2)
(define-fun _230 () Real (__BASE_ADDRESS_OF__ _229))
(define-fun _231 () Bool (= _229 _230))
(define-fun _232 () Real personOnFloor_4_2@2)
(define-fun _233 () Bool (= _232 _7))
(define-fun _234 () Bool (and _231 _233))
(define-fun _235 () Bool (and _228 _234))
(define-fun _236 () Real __ADDRESS_OF_personOnFloor_4_3)
(define-fun _237 () Real (__BASE_ADDRESS_OF__ _236))
(define-fun _238 () Bool (= _236 _237))
(define-fun _239 () Real personOnFloor_4_3@2)
(define-fun _240 () Bool (= _239 _7))
(define-fun _241 () Bool (and _238 _240))
(define-fun _242 () Bool (and _235 _241))
(define-fun _243 () Real __ADDRESS_OF_personOnFloor_4_4)
(define-fun _244 () Real (__BASE_ADDRESS_OF__ _243))
(define-fun _245 () Bool (= _243 _244))
(define-fun _246 () Real personOnFloor_4_4@2)
(define-fun _247 () Bool (= _246 _7))
(define-fun _248 () Bool (and _245 _247))
(define-fun _249 () Bool (and _242 _248))
(define-fun _250 () Real __ADDRESS_OF_personOnFloor_5_0)
(define-fun _251 () Real (__BASE_ADDRESS_OF__ _250))
(define-fun _252 () Bool (= _250 _251))
(define-fun _253 () Real personOnFloor_5_0@2)
(define-fun _254 () Bool (= _253 _7))
(define-fun _255 () Bool (and _252 _254))
(define-fun _256 () Bool (and _249 _255))
(define-fun _257 () Real __ADDRESS_OF_personOnFloor_5_1)
(define-fun _258 () Real (__BASE_ADDRESS_OF__ _257))
(define-fun _259 () Bool (= _257 _258))
(define-fun _260 () Real personOnFloor_5_1@2)
(define-fun _261 () Bool (= _260 _7))
(define-fun _262 () Bool (and _259 _261))
(define-fun _263 () Bool (and _256 _262))
(define-fun _264 () Real __ADDRESS_OF_personOnFloor_5_2)
(define-fun _265 () Real (__BASE_ADDRESS_OF__ _264))
(define-fun _266 () Bool (= _264 _265))
(define-fun _267 () Real personOnFloor_5_2@2)
(define-fun _268 () Bool (= _267 _7))
(define-fun _269 () Bool (and _266 _268))
(define-fun _270 () Bool (and _263 _269))
(define-fun _271 () Real __ADDRESS_OF_personOnFloor_5_3)
(define-fun _272 () Real (__BASE_ADDRESS_OF__ _271))
(define-fun _273 () Bool (= _271 _272))
(define-fun _274 () Real personOnFloor_5_3@2)
(define-fun _275 () Bool (= _274 _7))
(define-fun _276 () Bool (and _273 _275))
(define-fun _277 () Bool (and _270 _276))
(define-fun _278 () Real __ADDRESS_OF_personOnFloor_5_4)
(define-fun _279 () Real (__BASE_ADDRESS_OF__ _278))
(define-fun _280 () Bool (= _278 _279))
(define-fun _281 () Real personOnFloor_5_4@2)
(define-fun _282 () Bool (= _281 _7))
(define-fun _283 () Bool (and _280 _282))
(define-fun _284 () Bool (and _277 _283))
(define-fun _285 () Real __ADDRESS_OF_currentHeading)
(define-fun _286 () Real (__BASE_ADDRESS_OF__ _285))
(define-fun _287 () Bool (= _285 _286))
(define-fun _288 () Real currentHeading@2)
(define-fun _289 () Bool (= _288 _16))
(define-fun _290 () Bool (and _287 _289))
(define-fun _291 () Bool (and _284 _290))
(define-fun _292 () Real __ADDRESS_OF_currentFloorID)
(define-fun _293 () Real (__BASE_ADDRESS_OF__ _292))
(define-fun _294 () Bool (= _292 _293))
(define-fun _295 () Real currentFloorID@2)
(define-fun _296 () Bool (= _295 _7))
(define-fun _297 () Bool (and _294 _296))
(define-fun _298 () Bool (and _291 _297))
(define-fun _299 () Real __ADDRESS_OF_persons_0)
(define-fun _300 () Real (__BASE_ADDRESS_OF__ _299))
(define-fun _301 () Bool (= _299 _300))
(define-fun _302 () Real persons_0@2)
(define-fun _303 () Bool (= _302 _7))
(define-fun _304 () Bool (and _301 _303))
(define-fun _305 () Bool (and _298 _304))
(define-fun _306 () Real __ADDRESS_OF_persons_1)
(define-fun _307 () Real (__BASE_ADDRESS_OF__ _306))
(define-fun _308 () Bool (= _306 _307))
(define-fun _309 () Real persons_1@2)
(define-fun _310 () Bool (= _309 _7))
(define-fun _311 () Bool (and _308 _310))
(define-fun _312 () Bool (and _305 _311))
(define-fun _313 () Real __ADDRESS_OF_persons_2)
(define-fun _314 () Real (__BASE_ADDRESS_OF__ _313))
(define-fun _315 () Bool (= _313 _314))
(define-fun _316 () Real persons_2@2)
(define-fun _317 () Bool (= _316 _7))
(define-fun _318 () Bool (and _315 _317))
(define-fun _319 () Bool (and _312 _318))
(define-fun _320 () Real __ADDRESS_OF_persons_3)
(define-fun _321 () Real (__BASE_ADDRESS_OF__ _320))
(define-fun _322 () Bool (= _320 _321))
(define-fun _323 () Real persons_3@2)
(define-fun _324 () Bool (= _323 _7))
(define-fun _325 () Bool (and _322 _324))
(define-fun _326 () Bool (and _319 _325))
(define-fun _327 () Real __ADDRESS_OF_persons_4)
(define-fun _328 () Real (__BASE_ADDRESS_OF__ _327))
(define-fun _329 () Bool (= _327 _328))
(define-fun _330 () Real persons_4@2)
(define-fun _331 () Bool (= _330 _7))
(define-fun _332 () Bool (and _329 _331))
(define-fun _333 () Bool (and _326 _332))
(define-fun _334 () Real __ADDRESS_OF_persons_5)
(define-fun _335 () Real (__BASE_ADDRESS_OF__ _334))
(define-fun _336 () Bool (= _334 _335))
(define-fun _337 () Real persons_5@2)
(define-fun _338 () Bool (= _337 _7))
(define-fun _339 () Bool (and _336 _338))
(define-fun _340 () Bool (and _333 _339))
(define-fun _341 () Real __ADDRESS_OF_doorState)
(define-fun _342 () Real (__BASE_ADDRESS_OF__ _341))
(define-fun _343 () Bool (= _341 _342))
(define-fun _344 () Real doorState@2)
(define-fun _345 () Bool (= _344 _16))
(define-fun _346 () Bool (and _343 _345))
(define-fun _347 () Bool (and _340 _346))
(define-fun _348 () Real __ADDRESS_OF_floorButtons_0)
(define-fun _349 () Real (__BASE_ADDRESS_OF__ _348))
(define-fun _350 () Bool (= _348 _349))
(define-fun _351 () Real floorButtons_0@2)
(define-fun _352 () Bool (= _351 _7))
(define-fun _353 () Bool (and _350 _352))
(define-fun _354 () Bool (and _347 _353))
(define-fun _355 () Real __ADDRESS_OF_floorButtons_1)
(define-fun _356 () Real (__BASE_ADDRESS_OF__ _355))
(define-fun _357 () Bool (= _355 _356))
(define-fun _358 () Real floorButtons_1@2)
(define-fun _359 () Bool (= _358 _7))
(define-fun _360 () Bool (and _357 _359))
(define-fun _361 () Bool (and _354 _360))
(define-fun _362 () Real __ADDRESS_OF_floorButtons_2)
(define-fun _363 () Real (__BASE_ADDRESS_OF__ _362))
(define-fun _364 () Bool (= _362 _363))
(define-fun _365 () Real floorButtons_2@2)
(define-fun _366 () Bool (= _365 _7))
(define-fun _367 () Bool (and _364 _366))
(define-fun _368 () Bool (and _361 _367))
(define-fun _369 () Real __ADDRESS_OF_floorButtons_3)
(define-fun _370 () Real (__BASE_ADDRESS_OF__ _369))
(define-fun _371 () Bool (= _369 _370))
(define-fun _372 () Real floorButtons_3@2)
(define-fun _373 () Bool (= _372 _7))
(define-fun _374 () Bool (and _371 _373))
(define-fun _375 () Bool (and _368 _374))
(define-fun _376 () Real __ADDRESS_OF_floorButtons_4)
(define-fun _377 () Real (__BASE_ADDRESS_OF__ _376))
(define-fun _378 () Bool (= _376 _377))
(define-fun _379 () Real floorButtons_4@2)
(define-fun _380 () Bool (= _379 _7))
(define-fun _381 () Bool (and _378 _380))
(define-fun _382 () Bool (and _375 _381))
(define-fun _383 () Real |__ADDRESS_OF_main::tmp|)
(define-fun _384 () Real (__BASE_ADDRESS_OF__ _383))
(define-fun _385 () Bool (= _383 _384))
(define-fun _386 () Bool (and _382 _385))
(define-fun _387 () Real |__ADDRESS_OF_valid_product::retValue_acc|)
(define-fun _388 () Real (__BASE_ADDRESS_OF__ _387))
(define-fun _389 () Bool (= _387 _388))
(define-fun _390 () Bool (and _386 _389))
(define-fun _391 () Real |valid_product::retValue_acc@3|)
(define-fun _392 () Bool (= _391 _16))
(define-fun _393 () Bool (and _390 _392))
(define-fun _394 () Real |valid_product::__retval__@2|)
(define-fun _395 () Bool (= _391 _394))
(define-fun _396 () Bool (and _393 _395))
(define-fun _397 () Real |main::tmp@3|)
(define-fun _398 () Bool (= _394 _397))
(define-fun _399 () Bool (and _396 _398))
(define-fun _400 () Bool (= _397 _7))
(define-fun _403 () Bool (not _400))
(define-fun _404 () Bool (and _399 _403))
(define-fun _405 () Real |__ADDRESS_OF_bigMacCall::tmp|)
(define-fun _406 () Real (__BASE_ADDRESS_OF__ _405))
(define-fun _407 () Bool (= _405 _406))
(define-fun _408 () Bool (and _404 _407))
(define-fun _409 () Real 5)
(define-fun _410 () Real |getOrigin::person@2|)
(define-fun _411 () Bool (= _410 _409))
(define-fun _412 () Bool (and _408 _411))
(define-fun _413 () Real |__ADDRESS_OF_getOrigin::retValue_acc|)
(define-fun _414 () Real (__BASE_ADDRESS_OF__ _413))
(define-fun _415 () Bool (= _413 _414))
(define-fun _416 () Bool (and _412 _415))
(define-fun _417 () Bool (= _410 _7))
(define-fun _420 () Bool (not _417))
(define-fun _421 () Bool (and _416 _420))
(define-fun _422 () Bool (= _410 _16))
(define-fun _425 () Bool (not _422))
(define-fun _426 () Bool (and _421 _425))
(define-fun _427 () Real 2)
(define-fun _428 () Bool (= _410 _427))
(define-fun _431 () Bool (not _428))
(define-fun _432 () Bool (and _426 _431))
(define-fun _433 () Real 3)
(define-fun _434 () Bool (= _410 _433))
(define-fun _437 () Bool (not _434))
(define-fun _438 () Bool (and _432 _437))
(define-fun _439 () Bool (= _410 _27))
(define-fun _442 () Bool (not _439))
(define-fun _443 () Bool (and _438 _442))
(define-fun _445 () Bool (and _411 _443))
(define-fun _448 () Real |getOrigin::retValue_acc@3|)
(define-fun _449 () Bool (= _448 _16))
(define-fun _450 () Bool (and _445 _449))
(define-fun _451 () Real |getOrigin::__retval__@2|)
(define-fun _452 () Bool (= _448 _451))
(define-fun _453 () Bool (and _450 _452))
(define-fun _454 () Real |bigMacCall::tmp@3|)
(define-fun _455 () Bool (= _451 _454))
(define-fun _456 () Bool (and _453 _455))
(define-fun _457 () Real |initPersonOnFloor::person@2|)
(define-fun _458 () Bool (= _457 _409))
(define-fun _459 () Real |initPersonOnFloor::floor@2|)
(define-fun _460 () Bool (= _454 _459))
(define-fun _461 () Bool (and _458 _460))
(define-fun _462 () Bool (and _456 _461))
(define-fun _463 () Bool (= _459 _7))
(define-fun _466 () Bool (not _463))
(define-fun _467 () Bool (and _462 _466))
(define-fun _468 () Bool (= _459 _16))
(define-fun _470 () Bool (and _467 _468))
(define-fun _473 () Bool (= _457 _7))
(define-fun _476 () Bool (not _473))
(define-fun _477 () Bool (and _470 _476))
(define-fun _478 () Bool (= _457 _16))
(define-fun _481 () Bool (not _478))
(define-fun _482 () Bool (and _477 _481))
(define-fun _483 () Bool (= _457 _427))
(define-fun _486 () Bool (not _483))
(define-fun _487 () Bool (and _482 _486))
(define-fun _488 () Bool (= _457 _433))
(define-fun _491 () Bool (not _488))
(define-fun _492 () Bool (and _487 _491))
(define-fun _493 () Bool (= _457 _27))
(define-fun _496 () Bool (not _493))
(define-fun _497 () Bool (and _492 _496))
(define-fun _499 () Bool (and _458 _497))
(define-fun _502 () Real personOnFloor_5_1@3)
(define-fun _503 () Bool (= _502 _16))
(define-fun _504 () Bool (and _499 _503))
(define-fun _505 () Real |callOnFloor::floorID@2|)
(define-fun _506 () Bool (= _459 _505))
(define-fun _507 () Bool (and _504 _506))
(define-fun _508 () Bool (= _505 _7))
(define-fun _511 () Bool (not _508))
(define-fun _512 () Bool (and _507 _511))
(define-fun _513 () Bool (= _505 _16))
(define-fun _515 () Bool (and _512 _513))
(define-fun _518 () Real calls_1@3)
(define-fun _519 () Bool (= _518 _16))
(define-fun _520 () Bool (and _515 _519))
(define-fun _521 () Real |__ADDRESS_OF_timeShift::tmp|)
(define-fun _522 () Real (__BASE_ADDRESS_OF__ _521))
(define-fun _523 () Bool (= _521 _522))
(define-fun _524 () Bool (and _520 _523))
(define-fun _525 () Real |__ADDRESS_OF_timeShift::tmp___0|)
(define-fun _526 () Real (__BASE_ADDRESS_OF__ _525))
(define-fun _527 () Bool (= _525 _526))
(define-fun _528 () Bool (and _524 _527))
(define-fun _529 () Real |__ADDRESS_OF_timeShift::tmp___1|)
(define-fun _530 () Real (__BASE_ADDRESS_OF__ _529))
(define-fun _531 () Bool (= _529 _530))
(define-fun _532 () Bool (and _528 _531))
(define-fun _533 () Real |__ADDRESS_OF_timeShift::tmp___2|)
(define-fun _534 () Real (__BASE_ADDRESS_OF__ _533))
(define-fun _535 () Bool (= _533 _534))
(define-fun _536 () Bool (and _532 _535))
(define-fun _537 () Real |__ADDRESS_OF_timeShift::tmp___3|)
(define-fun _538 () Real (__BASE_ADDRESS_OF__ _537))
(define-fun _539 () Bool (= _537 _538))
(define-fun _540 () Bool (and _536 _539))
(define-fun _541 () Real |__ADDRESS_OF_timeShift::tmp___4|)
(define-fun _542 () Real (__BASE_ADDRESS_OF__ _541))
(define-fun _543 () Bool (= _541 _542))
(define-fun _544 () Bool (and _540 _543))
(define-fun _545 () Real |__ADDRESS_OF_timeShift::tmp___5|)
(define-fun _546 () Real (__BASE_ADDRESS_OF__ _545))
(define-fun _547 () Bool (= _545 _546))
(define-fun _548 () Bool (and _544 _547))
(define-fun _549 () Real |__ADDRESS_OF_timeShift::tmp___6|)
(define-fun _550 () Real (__BASE_ADDRESS_OF__ _549))
(define-fun _551 () Bool (= _549 _550))
(define-fun _552 () Bool (and _548 _551))
(define-fun _553 () Real |__ADDRESS_OF_timeShift::tmp___7|)
(define-fun _554 () Real (__BASE_ADDRESS_OF__ _553))
(define-fun _555 () Bool (= _553 _554))
(define-fun _556 () Bool (and _552 _555))
(define-fun _557 () Real |__ADDRESS_OF_timeShift::tmp___8|)
(define-fun _558 () Real (__BASE_ADDRESS_OF__ _557))
(define-fun _559 () Bool (= _557 _558))
(define-fun _560 () Bool (and _556 _559))
(define-fun _561 () Real |__ADDRESS_OF_timeShift::tmp___9|)
(define-fun _562 () Real (__BASE_ADDRESS_OF__ _561))
(define-fun _563 () Bool (= _561 _562))
(define-fun _564 () Bool (and _560 _563))
(define-fun _565 () Real |__ADDRESS_OF_stopRequestedAtCurrentFloor::retValue_acc|)
(define-fun _566 () Real (__BASE_ADDRESS_OF__ _565))
(define-fun _567 () Bool (= _565 _566))
(define-fun _568 () Bool (and _564 _567))
(define-fun _569 () Real |__ADDRESS_OF_stopRequestedAtCurrentFloor::tmp|)
(define-fun _570 () Real (__BASE_ADDRESS_OF__ _569))
(define-fun _571 () Bool (= _569 _570))
(define-fun _572 () Bool (and _568 _571))
(define-fun _573 () Real |__ADDRESS_OF_stopRequestedAtCurrentFloor::tmp___0|)
(define-fun _574 () Real (__BASE_ADDRESS_OF__ _573))
(define-fun _575 () Bool (= _573 _574))
(define-fun _576 () Bool (and _572 _575))
(define-fun _577 () Real |__ADDRESS_OF_isExecutiveFloorCalling::retValue_acc|)
(define-fun _578 () Real (__BASE_ADDRESS_OF__ _577))
(define-fun _579 () Bool (= _577 _578))
(define-fun _580 () Bool (and _576 _579))
(define-fun _581 () Real |isFloorCalling::floorID@2|)
(define-fun _582 () Bool (= _28 _581))
(define-fun _583 () Bool (and _580 _582))
(define-fun _584 () Real |__ADDRESS_OF_isFloorCalling::retValue_acc|)
(define-fun _585 () Real (__BASE_ADDRESS_OF__ _584))
(define-fun _586 () Bool (= _584 _585))
(define-fun _587 () Bool (and _583 _586))
(define-fun _588 () Bool (= _581 _7))
(define-fun _591 () Bool (not _588))
(define-fun _592 () Bool (and _587 _591))
(define-fun _593 () Bool (= _581 _16))
(define-fun _596 () Bool (not _593))
(define-fun _597 () Bool (and _592 _596))
(define-fun _598 () Bool (= _581 _427))
(define-fun _601 () Bool (not _598))
(define-fun _602 () Bool (and _597 _601))
(define-fun _603 () Bool (= _581 _433))
(define-fun _606 () Bool (not _603))
(define-fun _607 () Bool (and _602 _606))
(define-fun _608 () Bool (= _581 _27))
(define-fun _610 () Bool (and _607 _608))
(define-fun _613 () Real |isFloorCalling::retValue_acc@3|)
(define-fun _614 () Bool (= _71 _613))
(define-fun _615 () Bool (and _610 _614))
(define-fun _616 () Real |isFloorCalling::__retval__@2|)
(define-fun _617 () Bool (= _613 _616))
(define-fun _618 () Bool (and _615 _617))
(define-fun _619 () Real |isExecutiveFloorCalling::retValue_acc@3|)
(define-fun _620 () Bool (= _616 _619))
(define-fun _621 () Bool (and _618 _620))
(define-fun _622 () Real |isExecutiveFloorCalling::__retval__@2|)
(define-fun _623 () Bool (= _619 _622))
(define-fun _624 () Bool (and _621 _623))
(define-fun _625 () Real |stopRequestedAtCurrentFloor::tmp@3|)
(define-fun _626 () Bool (= _622 _625))
(define-fun _627 () Bool (and _624 _626))
(define-fun _628 () Bool (= _625 _7))
(define-fun _630 () Bool (and _627 _628))
(define-fun _633 () Real |__ADDRESS_OF_stopRequestedAtCurrentFloor__wrappee__base::retValue_acc|)
(define-fun _634 () Real (__BASE_ADDRESS_OF__ _633))
(define-fun _635 () Bool (= _633 _634))
(define-fun _636 () Bool (and _630 _635))
(define-fun _637 () Real |__ADDRESS_OF_stopRequestedAtCurrentFloor__wrappee__base::tmp|)
(define-fun _638 () Real (__BASE_ADDRESS_OF__ _637))
(define-fun _639 () Bool (= _637 _638))
(define-fun _640 () Bool (and _636 _639))
(define-fun _641 () Real |__ADDRESS_OF_stopRequestedAtCurrentFloor__wrappee__base::tmp___0|)
(define-fun _642 () Real (__BASE_ADDRESS_OF__ _641))
(define-fun _643 () Bool (= _641 _642))
(define-fun _644 () Bool (and _640 _643))
(define-fun _645 () Real |isFloorCalling::floorID@3|)
(define-fun _646 () Bool (= _295 _645))
(define-fun _647 () Bool (and _644 _646))
(define-fun _648 () Bool (and _586 _647))
(define-fun _649 () Bool (= _645 _7))
(define-fun _651 () Bool (and _648 _649))
(define-fun _654 () Real |isFloorCalling::retValue_acc@5|)
(define-fun _655 () Bool (= _43 _654))
(define-fun _656 () Bool (and _651 _655))
(define-fun _657 () Real |isFloorCalling::__retval__@3|)
(define-fun _658 () Bool (= _654 _657))
(define-fun _659 () Bool (and _656 _658))
(define-fun _660 () Real |stopRequestedAtCurrentFloor__wrappee__base::tmp___0@3|)
(define-fun _661 () Bool (= _657 _660))
(define-fun _662 () Bool (and _659 _661))
(define-fun _663 () Bool (= _660 _7))
(define-fun _665 () Bool (and _662 _663))
(define-fun _668 () Real |buttonForFloorIsPressed::floorID@2|)
(define-fun _669 () Bool (= _295 _668))
(define-fun _670 () Bool (and _665 _669))
(define-fun _671 () Real |__ADDRESS_OF_buttonForFloorIsPressed::retValue_acc|)
(define-fun _672 () Real (__BASE_ADDRESS_OF__ _671))
(define-fun _673 () Bool (= _671 _672))
(define-fun _674 () Bool (and _670 _673))
(define-fun _675 () Bool (= _668 _7))
(define-fun _677 () Bool (and _674 _675))
(define-fun _680 () Real |buttonForFloorIsPressed::retValue_acc@3|)
(define-fun _681 () Bool (= _351 _680))
(define-fun _682 () Bool (and _677 _681))
(define-fun _683 () Real |buttonForFloorIsPressed::__retval__@2|)
(define-fun _684 () Bool (= _680 _683))
(define-fun _685 () Bool (and _682 _684))
(define-fun _686 () Real |stopRequestedAtCurrentFloor__wrappee__base::tmp@3|)
(define-fun _687 () Bool (= _683 _686))
(define-fun _688 () Bool (and _685 _687))
(define-fun _689 () Bool (= _686 _7))
(define-fun _691 () Bool (and _688 _689))
(define-fun _694 () Real |stopRequestedAtCurrentFloor__wrappee__base::retValue_acc@3|)
(define-fun _695 () Bool (= _694 _7))
(define-fun _696 () Bool (and _691 _695))
(define-fun _697 () Real |stopRequestedAtCurrentFloor__wrappee__base::__retval__@2|)
(define-fun _698 () Bool (= _694 _697))
(define-fun _699 () Bool (and _696 _698))
(define-fun _700 () Real |stopRequestedAtCurrentFloor::retValue_acc@3|)
(define-fun _701 () Bool (= _697 _700))
(define-fun _702 () Bool (and _699 _701))
(define-fun _703 () Real |stopRequestedAtCurrentFloor::__retval__@2|)
(define-fun _704 () Bool (= _700 _703))
(define-fun _705 () Bool (and _702 _704))
(define-fun _706 () Real |timeShift::tmp___9@3|)
(define-fun _707 () Bool (= _703 _706))
(define-fun _708 () Bool (and _705 _707))
(define-fun _709 () Bool (= _706 _7))
(define-fun _711 () Bool (and _708 _709))
(define-fun _715 () Bool (and _345 _711))
(define-fun _718 () Real doorState@3)
(define-fun _719 () Bool (= _718 _7))
(define-fun _720 () Bool (and _715 _719))
(define-fun _721 () Real |stopRequestedInDirection::dir@2|)
(define-fun _722 () Bool (= _288 _721))
(define-fun _723 () Real |stopRequestedInDirection::respectFloorCalls@2|)
(define-fun _724 () Bool (= _723 _16))
(define-fun _725 () Bool (and _722 _724))
(define-fun _726 () Real |stopRequestedInDirection::respectInLiftCalls@2|)
(define-fun _727 () Bool (= _726 _16))
(define-fun _728 () Bool (and _725 _727))
(define-fun _729 () Bool (and _720 _728))
(define-fun _730 () Real |__ADDRESS_OF_stopRequestedInDirection::retValue_acc|)
(define-fun _731 () Real (__BASE_ADDRESS_OF__ _730))
(define-fun _732 () Bool (= _730 _731))
(define-fun _733 () Bool (and _729 _732))
(define-fun _734 () Real |__ADDRESS_OF_stopRequestedInDirection::tmp|)
(define-fun _735 () Real (__BASE_ADDRESS_OF__ _734))
(define-fun _736 () Bool (= _734 _735))
(define-fun _737 () Bool (and _733 _736))
(define-fun _738 () Real |__ADDRESS_OF_stopRequestedInDirection::tmp___0|)
(define-fun _739 () Real (__BASE_ADDRESS_OF__ _738))
(define-fun _740 () Bool (= _738 _739))
(define-fun _741 () Bool (and _737 _740))
(define-fun _742 () Real |__ADDRESS_OF_stopRequestedInDirection::__cil_tmp7|)
(define-fun _743 () Real (__BASE_ADDRESS_OF__ _742))
(define-fun _744 () Bool (= _742 _743))
(define-fun _745 () Bool (and _741 _744))
(define-fun _746 () Real |__ADDRESS_OF_stopRequestedInDirection::__cil_tmp8|)
(define-fun _747 () Real (__BASE_ADDRESS_OF__ _746))
(define-fun _748 () Bool (= _746 _747))
(define-fun _749 () Bool (and _745 _748))
(define-fun _750 () Bool (and _579 _749))
(define-fun _751 () Real |isFloorCalling::floorID@4|)
(define-fun _752 () Bool (= _28 _751))
(define-fun _753 () Bool (and _750 _752))
(define-fun _754 () Bool (and _586 _753))
(define-fun _755 () Bool (= _751 _7))
(define-fun _758 () Bool (not _755))
(define-fun _759 () Bool (and _754 _758))
(define-fun _760 () Bool (= _751 _16))
(define-fun _763 () Bool (not _760))
(define-fun _764 () Bool (and _759 _763))
(define-fun _765 () Bool (= _751 _427))
(define-fun _768 () Bool (not _765))
(define-fun _769 () Bool (and _764 _768))
(define-fun _770 () Bool (= _751 _433))
(define-fun _773 () Bool (not _770))
(define-fun _774 () Bool (and _769 _773))
(define-fun _775 () Bool (= _751 _27))
(define-fun _777 () Bool (and _774 _775))
(define-fun _780 () Real |isFloorCalling::retValue_acc@7|)
(define-fun _781 () Bool (= _71 _780))
(define-fun _782 () Bool (and _777 _781))
(define-fun _783 () Real |isFloorCalling::__retval__@4|)
(define-fun _784 () Bool (= _780 _783))
(define-fun _785 () Bool (and _782 _784))
(define-fun _786 () Real |isExecutiveFloorCalling::retValue_acc@5|)
(define-fun _787 () Bool (= _783 _786))
(define-fun _788 () Bool (and _785 _787))
(define-fun _789 () Real |isExecutiveFloorCalling::__retval__@3|)
(define-fun _790 () Bool (= _786 _789))
(define-fun _791 () Bool (and _788 _790))
(define-fun _792 () Real |stopRequestedInDirection::tmp___0@3|)
(define-fun _793 () Bool (= _789 _792))
(define-fun _794 () Bool (and _791 _793))
(define-fun _795 () Bool (= _792 _7))
(define-fun _797 () Bool (and _794 _795))
(define-fun _800 () Real |stopRequestedInDirection__wrappee__base::dir@2|)
(define-fun _801 () Bool (= _721 _800))
(define-fun _802 () Real |stopRequestedInDirection__wrappee__base::respectFloorCalls@2|)
(define-fun _803 () Bool (= _723 _802))
(define-fun _804 () Bool (and _801 _803))
(define-fun _805 () Real |stopRequestedInDirection__wrappee__base::respectInLiftCalls@2|)
(define-fun _806 () Bool (= _726 _805))
(define-fun _807 () Bool (and _804 _806))
(define-fun _808 () Bool (and _797 _807))
(define-fun _809 () Real |__ADDRESS_OF_stopRequestedInDirection__wrappee__base::retValue_acc|)
(define-fun _810 () Real (__BASE_ADDRESS_OF__ _809))
(define-fun _811 () Bool (= _809 _810))
(define-fun _812 () Bool (and _808 _811))
(define-fun _813 () Real |__ADDRESS_OF_stopRequestedInDirection__wrappee__base::tmp|)
(define-fun _814 () Real (__BASE_ADDRESS_OF__ _813))
(define-fun _815 () Bool (= _813 _814))
(define-fun _816 () Bool (and _812 _815))
(define-fun _817 () Real |__ADDRESS_OF_stopRequestedInDirection__wrappee__base::tmp___0|)
(define-fun _818 () Real (__BASE_ADDRESS_OF__ _817))
(define-fun _819 () Bool (= _817 _818))
(define-fun _820 () Bool (and _816 _819))
(define-fun _821 () Real |__ADDRESS_OF_stopRequestedInDirection__wrappee__base::tmp___1|)
(define-fun _822 () Real (__BASE_ADDRESS_OF__ _821))
(define-fun _823 () Bool (= _821 _822))
(define-fun _824 () Bool (and _820 _823))
(define-fun _825 () Real |__ADDRESS_OF_stopRequestedInDirection__wrappee__base::tmp___2|)
(define-fun _826 () Real (__BASE_ADDRESS_OF__ _825))
(define-fun _827 () Bool (= _825 _826))
(define-fun _828 () Bool (and _824 _827))
(define-fun _829 () Real |__ADDRESS_OF_stopRequestedInDirection__wrappee__base::tmp___3|)
(define-fun _830 () Real (__BASE_ADDRESS_OF__ _829))
(define-fun _831 () Bool (= _829 _830))
(define-fun _832 () Bool (and _828 _831))
(define-fun _833 () Real |__ADDRESS_OF_stopRequestedInDirection__wrappee__base::tmp___4|)
(define-fun _834 () Real (__BASE_ADDRESS_OF__ _833))
(define-fun _835 () Bool (= _833 _834))
(define-fun _836 () Bool (and _832 _835))
(define-fun _837 () Real |__ADDRESS_OF_stopRequestedInDirection__wrappee__base::tmp___5|)
(define-fun _838 () Real (__BASE_ADDRESS_OF__ _837))
(define-fun _839 () Bool (= _837 _838))
(define-fun _840 () Bool (and _836 _839))
(define-fun _841 () Real |__ADDRESS_OF_stopRequestedInDirection__wrappee__base::tmp___6|)
(define-fun _842 () Real (__BASE_ADDRESS_OF__ _841))
(define-fun _843 () Bool (= _841 _842))
(define-fun _844 () Bool (and _840 _843))
(define-fun _845 () Real |__ADDRESS_OF_stopRequestedInDirection__wrappee__base::tmp___7|)
(define-fun _846 () Real (__BASE_ADDRESS_OF__ _845))
(define-fun _847 () Bool (= _845 _846))
(define-fun _848 () Bool (and _844 _847))
(define-fun _849 () Real |__ADDRESS_OF_stopRequestedInDirection__wrappee__base::tmp___8|)
(define-fun _850 () Real (__BASE_ADDRESS_OF__ _849))
(define-fun _851 () Bool (= _849 _850))
(define-fun _852 () Bool (and _848 _851))
(define-fun _853 () Real |__ADDRESS_OF_stopRequestedInDirection__wrappee__base::tmp___9|)
(define-fun _854 () Real (__BASE_ADDRESS_OF__ _853))
(define-fun _855 () Bool (= _853 _854))
(define-fun _856 () Bool (and _852 _855))
(define-fun _857 () Bool (= _800 _16))
(define-fun _859 () Bool (and _856 _857))
(define-fun _862 () Real |isTopFloor::floorID@2|)
(define-fun _863 () Bool (= _295 _862))
(define-fun _864 () Bool (and _859 _863))
(define-fun _865 () Real |__ADDRESS_OF_isTopFloor::retValue_acc|)
(define-fun _866 () Real (__BASE_ADDRESS_OF__ _865))
(define-fun _867 () Bool (= _865 _866))
(define-fun _868 () Bool (and _864 _867))
(define-fun _869 () Bool (= _862 _27))
(define-fun _870 () Real (ite _869 _16 _7))
(define-fun _871 () Real |isTopFloor::retValue_acc@3|)
(define-fun _872 () Bool (= _870 _871))
(define-fun _873 () Bool (and _868 _872))
(define-fun _874 () Real |isTopFloor::__retval__@2|)
(define-fun _875 () Bool (= _871 _874))
(define-fun _876 () Bool (and _873 _875))
(define-fun _877 () Real |stopRequestedInDirection__wrappee__base::tmp@3|)
(define-fun _878 () Bool (= _874 _877))
(define-fun _879 () Bool (and _876 _878))
(define-fun _880 () Bool (= _877 _7))
(define-fun _882 () Bool (and _879 _880))
(define-fun _885 () Bool (<= _7 _295))
(define-fun _889 () Bool (and _882 _885))
(define-fun _891 () Bool (and _885 _889))
(define-fun _892 () Bool (<= _16 _295))
(define-fun _893 () Bool (not _892))
(define-fun _895 () Bool (and _891 _893))
(define-fun _897 () Bool (= _802 _7))
(define-fun _900 () Bool (not _897))
(define-fun _901 () Bool (and _895 _900))
(define-fun _902 () Real ___pc@4)
(define-fun _903 () Bool (= _902 _35))
(define-fun _904 () Bool (and _901 _903))


(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(push 1)
(assert _904)
(set-info :status sat)
(check-sat)
(pop 1)
(exit)
